定期ミートアップ　第6回　takoeight0821

前回の振り返り

Malgoでプログラムを書いてたら、とんでもないことに気づいた

パターンマッチに漏れがあると未定義動作になる

code:UB.mlg

data List a = Nil | Cons a (List a);

-- リスト長が1以外のときの動作が未定義

ub = { Cons x Nil -> x };

本当は部分関数になってほしいのに、最適化するとただのheadになってしまう！

ググるとSwiftで使われているらしいアルゴリズムの論文がヒットした（元はScala？）

Fengyun Liu. 2016. A generic algorithm for checking exhaustivity of pattern matching

LIU2016のアイディアのミソ

スペースはカバーしている値の集合

P(Nil) = K(Nil)

P(Cons x Nil) = K(Cons, T(typeof(x)), K(Nil))

型のスペース - パターンのスペースが空　ならば　型のスペース ⊆ パターンのスペース

スペースの差を考える理由

ユーザフレンドリなコンパイラは、反例を示すためにどちらにせよスペースの差を求める必要がある

code:スペースの差の計算

型のスペース - パターンのスペース

T(List a) - K(Nil)

= (K(Nil) | K(Cons, T(a), T(List a))) - K(Nil)

= K(Cons, T(a), T(List a)) Cons x xsのパターンが足りない！

Malgoへの実装

次のスクショのように、網羅的でないパターンを警告してくれる

HEADでは網羅的でないパターンをコンパイルエラーとして扱う（パターンは必ず網羅的でないといけない）

将来的にどうするかは考え中。オプションで警告に格下げ&実行時例外を投げるとか？

code:hoge

data Option a = None | Some a

lookupCache |> { Err x -> print x

| Ok -> read |> print }

if let Some(x) = lookupCache {

}

仕込んだバグ

再帰しているので素朴にやると無限ループになる。差を計算するときに必要に応じて展開するように修正した

LIU2016にもそう書いてあった。定義はきちんと読みましょう。

エラー行の出力のコードにまぬけなミスが

深夜に書いた賢いコードは往々にして間違ってる……

code:error

ただしい出力

|

338 | tail = { Cons _ xs -> xs };

|

実際の出力

|

338 | tail = { Cons _ xs -> xs };

|

補足

Q:定数パターンのスペースってどうするの？

LIU2016では、"We have extended the approach to introduce a concept called point in order to support constants, Java enumerations and stable identifiers in patterns. The extension is straight-forward and trivial to implement."と書かれている（Scalaコンパイラ）

dottyの実装を見ると、定数パターンのスペースをconstant typeのスペースとして扱っているっぽい

詳細はわからず……（誰か教えて下さい）

定数パターンがあるパターンマッチでは、実用上必ずdefault節が必要になる

P(0) = {}なら、T(Int32) - P(0) = T(Int32)となり、default節が足りていないことがわかる

Malgoの実装はこの方針

定数が有限個の型、例えば真偽値リテラルのパターンとかは空にせず、コンストラクタパターンと同様に扱う

もっと複雑なパターン（view patternやguard）をサポートするには、もう少し込み入ったことをする必要がありそう

Haskell（GHC）では、最近 Lower Your Guardsというのが出た

エキゾチックなパターンの網羅性を正しく検査したい、という話らしい

code:safeLast.hs

safeLast (reverse -> (x : )) = Just x